$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:fpf($A$; $x$.$B$($x$)), $C$:Type, $a$:($A$$\rightarrow$(?$C$)), $b$:($C$$\rightarrow$$A$).
\\[0ex]($\forall$$y$:$A$. ($\uparrow$isl($a$($y$))) $\Rightarrow$ ($b$(outl($a$($y$))) = $y$)) $\Rightarrow$ (compose{-}fpf($a$; $b$; $f$) $\in$ fpf($C$; $y$.$B$($b$($y$))))